(set-logic BV)

(define-fun shr1 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000001))
(define-fun shr4 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000004))
(define-fun shr16 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000010))
(define-fun shl1 ((x (BitVec 64))) (BitVec 64) (bvshl x #x0000000000000001))
(define-fun if0 ((x (BitVec 64)) (y (BitVec 64)) (z (BitVec 64))) (BitVec 64) (ite (= x #x0000000000000001) y z))

(synth-fun f ( (x (BitVec 64))) (BitVec 64)
(

(Start (BitVec 64) (#x0000000000000000 #x0000000000000001 x (bvnot Start)
                    (shl1 Start)
 		    (shr1 Start)
		    (shr4 Start)
		    (shr16 Start)
		    (bvand Start Start)
		    (bvor Start Start)
		    (bvxor Start Start)
		    (bvadd Start Start)
		    (if0 Start Start Start)
 ))
)
)
(constraint (= (f #x77F6D3587D33F8AC) #x0000EFEDA6B0FA67))
(constraint (= (f #xBA126A4C3CAF8326) #x00007424D498795F))
(constraint (= (f #x1C9CFA1FA96D95DE) #x00003939F43F52DB))
(constraint (= (f #xAE01303465C381AC) #x00005C026068CB87))
(constraint (= (f #x984EE90F3B3597BD) #x0000309DD21E766B))
(constraint (= (f #xD47F048B4E3B2222) #x0000A8FE09169C76))
(constraint (= (f #x8EF5924F1EE500EA) #x00001DEB249E3DCA))
(constraint (= (f #xE8047A86DE8704AB) #x0000D008F50DBD0E))
(constraint (= (f #xB2DDAD0AB759417B) #x000065BB5A156EB2))
(constraint (= (f #xBE2BE74998777D72) #x00007C57CE9330EE))
(constraint (= (f #xFFFFFFFFFFFFFFC5) #x0000FFFFFFFFFFFF))
(constraint (= (f #xFFFFFFFFFFFFFFD4) #x0000FFFFFFFFFFFF))
(constraint (= (f #xFFFFFFFFFFFFFFD2) #x0000FFFFFFFFFFFF))
(constraint (= (f #xFFFFFFFFFFFFFFD8) #x0000FFFFFFFFFFFF))
(constraint (= (f #xFFFFFFFFFFFFFFD0) #x0000FFFFFFFFFFFF))
(constraint (= (f #x0D2660D34C2AC659) #x03499834D30AB196))
(constraint (= (f #x73DF9C9F2A37FFFF) #x1CF7E727CA8E0000))
(constraint (= (f #x91FAF3662A6ACDA5) #x247EBCD98A9AB369))
(constraint (= (f #xE734B6B141D2C0FD) #x39CD2DAC5074B03F))
(constraint (= (f #xFB2FBBCD5F40DAFA) #x3ECBEEF357D036BE))
(constraint (= (f #x340A096B61DA6088) #x0D02825AD8769822))
(constraint (= (f #x9E186459E52E051A) #x27861916794B8146))
(constraint (= (f #x86560BC21A7214CA) #x219582F0869C8532))
(constraint (= (f #x1715825E243404FD) #x05C56097890D013F))
(constraint (= (f #xD6640B2B2DF26C9D) #x359902CACB7C9B27))
(constraint (= (f #x0000000000000000) #x0000000000000000))
(check-synth)
